Nuprl Lemma : ldst_wf 0,22
l:IdLnk. destination(l)  Id 
latex

DefinitionsIdLnk, destination(l), 1of(t), 2of(t), x. t(x), x:A. B(x), Id, t  T,
Lemmasnat wf, Id wf, pi2 wf, pi1 wf

origin